Nuprl Lemma : length-map-sq
11,40
postcript
pdf
f
:Top,
L
:(Top List). ||map(
f
;
L
)|| ~ ||
L
||
latex
Definitions
t
T
,
x
:
A
.
B
(
x
)
,
x
:
A
B
(
x
)
,
type
List
,
s
~
t
,
Top
Lemmas
length-map
,
top
wf
origin
f:Top, L:(Top List). ||map(f;L)|| ~ ||L|| f:Top, L:(Top List). ||map(f;L)|| ~ ||L|| 
Tx:A. B(x)
B(x)